package cfsmon.logic.nfm;

import java.util.Collections;
import java.util.HashMap;
import java.util.HashSet;
import java.util.LinkedList;
import java.util.Map;
import java.util.Queue;
import java.util.Set;

import org.apache.log4j.Logger;

import cfsmon.common.Event;
import cfsmon.logic.dfm.Dfm;
import cfsmon.logic.dfm.DfmState;
import cfsmon.logic.dfm.IDfm;

/**
 * Definition: A transition (s,e,s') is constructing if and only if
 * s in initialStates and (e in Events, s' in initialStates U finalStates
 * or e has all parameters of the nfm).
 * @author Alexander Gebhardt
 */
public class NfmToDfmTranslator {

	private static Logger logger = Logger.getLogger(NfmToDfmTranslator.class);
	
	/**
	 * Transforms a NFM into a DFM using either a simple transformation or the
	 * powerset construction. The NFM to transform is required to have a total
	 * transition relation, i.e. for every state and every event exists a defined
	 * target state.
	 * @param nfm The NFM to transform
	 * @return A DFM
	 */
	public static IDfm translateToDfm(INfm nfm){
		if (nfm != null){
			logger.info("Performing NFM to DFM translation.");
			if (isAlreadyDeterministic(nfm)){
				logger.info("Detected DFM as input. Performing simple conversion.");
				return makeDeterministicSimple(nfm);
			} else {
				logger.info("Detected NFM as input. Performing powerset conversion.");
				return makeDeterministic(nfm);				
			}
		}
		else
			return null;
	}
	
	private static boolean isAlreadyDeterministic(INfm nfm){
		
		if (nfm.getInitialStates().size() > 1)
			return false;
		
		for (NfmState s : nfm.getStates().values()){
			for (Set<NfmState> to : s.getTransitions().values()){
				if (to.size() > 1)
					return false;
			}
			if (s.getDefaultTransition().size() > 1)
				return false;
		}
		
		return true;
	}
	
	private static IDfm makeDeterministicSimple(INfm nfm){
		IDfm dfm = new Dfm();
		
		// parameters
		dfm.getParameters().putAll(nfm.getParameters());
		
		// events
		dfm.getEvents().putAll(nfm.getEvents());
		
		// maximum monitors
		dfm.setMaximumNumberOfMonitors(nfm.getMaximumNumberOfMonitors());
		
		// states
		for (NfmState nFrom : nfm.getStates().values()){
			DfmState dFrom = dfm.getStates().get(nFrom.getName());
			if (dFrom == null){
				dFrom = new DfmState(nFrom.getName());
				dfm.addState(dFrom);
			}
			// event transitions
			for (Event e : nFrom.getTransitions().keySet()){
				for (NfmState nTo : nFrom.getTransitions().get(e)){
					DfmState dTo = dfm.getStates().get(nTo.getName());
					if (dTo == null){
						dTo = new DfmState(nTo.getName());
						dfm.addState(dTo);
					}
					dFrom.putTransition(e, dTo);
					break;
				}
			}
			// default transition
			for (NfmState nTo : nFrom.getDefaultTransition()){
				DfmState dTo = dfm.getStates().get(nTo.getName());
				if (dTo == null){
					dTo = new DfmState(nTo.getName());
					dfm.addState(dTo);
				}
				dFrom.setDefaultTransition(dTo);
				break;
			}
		}
		
		// initial state
		for (NfmState nInit : nfm.getInitialStates()){
			DfmState dInit = dfm.getStates().get(nInit.getName());
			if (dInit == null){
				dInit = new DfmState(nInit.getName());
				dfm.addState(dInit);
			}
			dfm.setInitialState(dInit);
			break;
		}
		
		// final states
		for (NfmState nFinal : nfm.getFinalStates()){
			DfmState dFinal = dfm.getStates().get(nFinal.getName());
			if (dFinal == null){
				dFinal = new DfmState(nFinal.getName());
				dfm.addState(dFinal);
			}
			dfm.addFinalState(dFinal);
		}
		
		return dfm;
	}
	
	/**
	 * Powerset construction 
	 */
	private static IDfm makeDeterministic(INfm nfm){
		
		IDfm dfm = new Dfm();
		
		boolean nontotal = false;
		
		dfm.getParameters().putAll(nfm.getParameters());
		dfm.getEvents().putAll(nfm.getEvents());
		
		dfm.setMaximumNumberOfMonitors(nfm.getMaximumNumberOfMonitors());
		
		Map<Set<NfmState>, DfmState> powersetStateMap = new HashMap<Set<NfmState>, DfmState>();
		
		dfm.setInitialState(new DfmState()); // s0
		
		Queue<Set<NfmState>> unvisitedPowersets = new LinkedList<Set<NfmState>>();
		
		// add initial state (no epsilon transitions in the input language, i.e.
		// the set of initial states is the initial state of the powerset construction)
		unvisitedPowersets.add(nfm.getInitialStates());
		powersetStateMap.put(nfm.getInitialStates(), dfm.getInitialState());
		
		Set<NfmState> currentPowerset = null, nextPowerset = null;
		DfmState currentState = null, nextState = null;
		
		while (!unvisitedPowersets.isEmpty()){
			currentPowerset = unvisitedPowersets.poll();
			currentState = powersetStateMap.get(currentPowerset);
			
			for (Event e : nfm.getEvents().values()){
				nextPowerset = moveNondeterministic(currentPowerset, e);
				if (!nontotal && nextPowerset.isEmpty()){
					nontotal = true;
					logger.warn("Non-total transition relation detected. A dummy state wil be inserted.");
				}
				nextState = powersetStateMap.get(nextPowerset);
				if (nextState == null){
					// discovered a new state
					nextState = new DfmState();
					powersetStateMap.put(nextPowerset, nextState);
					unvisitedPowersets.add(nextPowerset);
					dfm.addState(nextState);
					if (!Collections.disjoint(nextPowerset, nfm.getFinalStates())){
						dfm.addFinalState(nextState);
					}
				}
				currentState.putTransition(e, nextState);
			}
		}
		
		return dfm;
		// Pseudocode:
		// dfmZustand fuer initialSet erstellen (map:set->zustand) und in die queue als unbearbeitet einfuegen
		// zustand als startzustand festhalten
		// solange unbearbeitete sets nicht leer
		// 	hole erstes unbearbeitetes set S aus der queue (poll)
		//	hole zustand s mit (S,s) aus der map
		//	fuer jedes eingabesymbol e:
		//		ermittle folgezustandsmenge S'
		//		falls s' mit (S',s') nicht existiert,
		//			fuege (S',s') in die map ein
		//			fuege S' an die queue an
		//			falls S' und finalStates nicht disjunkt,
		//				fuege s' der Menge der Endzustaende hinzu.
		//		fuege (s,e,s') als transition hinzu
		// im dfa sind die default-transitionen allesamt reflexiv
	}
	
	/**
	 * Returns the set of states the nfm changes to via input e.
	 * @param currentState The current nfm state set
	 * @param e An input symbol / event
	 * @return The resulting state set
	 */
	private static Set<NfmState> moveNondeterministic(Set<NfmState> currentState, Event e){
		Set<NfmState> nextState, tmp;
		nextState = new HashSet<NfmState>();
		for (NfmState s : currentState){
			tmp = s.getTransitions().get(e);
			if (tmp == null || tmp.isEmpty()){
				// event triggers default transition
				nextState.addAll(s.getDefaultTransition());
			} else {
				// event triggers event transition
				nextState.addAll(tmp);				
			}
		}
		return nextState;
	}
}
